The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
subtrees(@t) → subtrees#1(@t)
subtrees#1(leaf) → nil
subtrees#1(node(@x, @t1, @t2)) → subtrees#2(subtrees(@t1), @t1, @t2, @x)
subtrees#2(@l1, @t1, @t2, @x) → subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
subtrees#3(@l2, @l1, @t1, @t2, @x) → ::(node(@x, @t1, @t2), append(@l1, @l2))

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
append(::(@x3_0, @xs4_0), @l2) →⁺ ::(@x3_0, append(@xs4_0, @l2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs4_0 / ::(@x3_0, @xs4_0)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)